COMMENT ⊗   VALID 00010 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notion of multiplicity
C00006 00003	multiplicity of union is sum of multiplicities
C00007 00004	PROOFS
C00008 00005	proof of facts about mult
C00010 00006	mult_nthcdr
C00012 00007	lemma multiplicity implies injectivity: a sublemma
C00015 00008	lemma multiplicity implies injectivity
C00017 00009	proof multsum                                
C00019 00010	Lemma:if disjoint-set,then multiplicity of union = sum of the multiplicities
C00021 ENDMK
C⊗;
;the notion of multiplicity

(wipe-out)
(get-proofs sums prf ekl sys)

(proof multiplicity)

(decl mult (type: |(ground⊗@set)→ground|) (syntype: constant))
(defax mult |∀x u a.mult(nil,a)=0∧
                    mult(x.u,a)=if a(x) then mult(u,a)' else mult(u,a)|)
(label mult_def)

;facts about multiplicity

(axiom |∀u a.natnum(mult(u,a))|)
(label simpinfo)(label multfact)

(axiom |∀u a.mult(u,a)≤length(u)|)
(label length_mult)

(axiom |∀u y a.member(y,u)∧a(y)⊃1≤mult(u,a)|) 
(label member_mult)

;Exercise:(not used in the proofs)
;(axiom |∀a u x.mult(u,a)≤mult(x.u,a)|)
;(label simpinfo)(label multfact)

(axiom |∀a u n.n<length(u)⊃mult(nthcdr(u,n),a)≤mult(u,a)|)
(label mult_nthcdr)

(axiom |∀u.mult(u,emptyset)=0|)
(label simpinfo)(label emptyfacts)

(axiom |∀v i j.i<j∧j<length v∧nth(v,i)=nth(v,j)⊃
               2≤mult(v,mkset(nth(v,i)))|)
(label multinj_computation)

(axiom |∀v.(∀k.k<length v⊃mult(v,mkset(nth(v,k)))=1)⊃inj(v)|)
(label mult_inj)
;multiplicity of union is sum of multiplicities
(proof mult_of_un_is_sum_un)

(axiom |∀u a b.disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|)
(label multsum)

(axiom |∀setseq u n.disjoint(setseq,n)⊃
                    mult(u,un(setseq,n))=sum(λm.mult(u,setseq(m)),n)|)
(label mult_of_un_is_sum_mult)
(save-proofs mult)
;PROOFS
;proof of facts about mult
    (wipe-out)
    (get-proofs mult prf ekl sys)
    (proof multprop)
    (unlabel simpinfo multfact)

1.  (ue (phi |λu.∀a.natnum(mult(u,a))|) listinduction 
	(use mult_def mode: always))

    (label simpinfo multfact)

    ;not used later in the proofs
    ;(trw |∀a u x.mult(u,a)≤mult(x.u,a)| (open mult lesseq) (use successor1))
    ;∀A U X.mult(U,A)≤mult(X.U,A)

    ;multiplicity is lesseq length

2.  (ue (phi |λu.mult(u,a)≤length(u)|) listinduction 
	lesseq_lesseq_succ (open mult length) (part 1#1(open lesseq)))
    ;∀U.MULT(U,A)≤LENGTH U

    ;if there is a member, multiplicity is not zero

3.  (ue (phi |λu.∀y a.member(y,u)∧a(y)⊃0<mult(u,a)|) listinduction 
	(open mult member) (use normal mode: always))
    ;∀U Y A.MEMBER(Y,U)∧A(Y)⊃0<MULT(U,A)

4.  (rw * use less_lesseqsucc mode: always))
    ;∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)

    ;mult emptyset
    (unlabel simpinfo emptyfacts)

5.  (ue (phi |λu.mult(u,emptyset)=0|) listinduction 
	(part 1(open emptyset mult)))
    ;∀U.MULT(U,EMPTYSET)=0
    (label simpinfo emptyfacts)
;mult_nthcdr

    ;we prepare a rewriter


6.  (ue ((q.|mult(nthcdr(u,n'),a)'≤mult(u,a)|)
	 (r.|mult(nthcdr(u,n'),a)≤mult(u,a)|)
	 (p.|a(nth(u,n))|)) trans_cond
	(use succ_lesseq_lesseq ue: ((m.|mult(nthcdr(u,n'),a)|)
				     (n.|mult(u,a)|)) mode: exact ))
    ;(IF A(NTH(U,N)) THEN MULT(NTHCDR(U,N'),A)'≤MULT(U,A)
    ;    ELSE MULT(NTHCDR(U,N'),A)≤MULT(U,A))⊃MULT(NTHCDR(U,N'),A)≤MULT(U,A)

    ;conclusion

7.  (ue (a |λn.∀a u.n<length(u)⊃mult(nthcdr(u,n),a)≤mult(u,a)|) proof_by_induction
	(part 1#1 (open nthcdr lesseq)) succ_less_less 
	(part 1#2#1#1 (use nthcdr_car_cdr mode: always)) (open mult)   *)
    ;∀N A U.N<LENGTH U⊃MULT(NTHCDR(U,N),A)≤MULT(U,A)

;lemma multiplicity implies injectivity: a sublemma
;to compute multiplicity

    (wipe-out)
    (get-proofs mult prf ekl sys)
    (proof multinj_computation)

1.  (assume |j<length v|)
    (label mc0)

2.  (assume |i<j|)
    (label mc1)

3.  (assume |nth(v,i)=nth(v,j)|)
    (label mc2)

4.  (derive |i<length v| (mc0 mc1 transitivity_of_order))
    (label mc3)
    ;deps: (mc0 mc1)

    ;labels: NTH_IN_NTHCDR 
    ;(AXIOM |∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))|)

5.  (ue ((u.v)(n.|i'|)(m.j)) nth_in_nthcdr mc0 mc1 
        (use less_lesseqsucc mode: exact direction: reverse))
    ;MEMBER(NTH(V,J),NTHCDR(V,I'))
    (label mc4)
    ;deps: (MC0 MC1)

    ;labels: MEMBER_MULT 
    ;∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)

6.  (ue ((u.|nthcdr(v,i')|)(y.|nth(v,j)|)(a.|mkset nth(v,j)|)) member_mult 
        (part 1(open lesseq mkset)) mc4
        (use mc2 mode: exact direction: reverse)) 
    ;1≤MULT(NTHCDR(V,I'),MKSET(NTH(V,I)))
    (label mc5)
    ;deps: (MC0 MC1 MC2)

7.  (trw |n≤mult(nthcdr(v,i'),mkset nth(v,i))⊃n'≤mult(nthcdr(v,i),mkset nth(v,i))| 
         (open mult mkset)(use nthcdr_car_cdr mc3 mode: exact))
    ;N≤MULT(NTHCDR(V,I'),MKSET(NTH(V,I)))⊃N'≤MULT(NTHCDR(V,I),MKSET(NTH(V,I)))
    ;deps: (MC0 MC1)

8.  (ue (n |1|) * mc5)
    ;2≤MULT(NTHCDR(V,I),MKSET(NTH(V,I)))
    (label mc6)
    ;deps: (MC0 MC1 MC2)

    ;labels: MULT_NTHCDR 
    ;(AXIOM |∀A U N.N<LENGTH U⊃MULT(NTHCDR(U,N),A)≤MULT(U,A)|)

9.  (ue ((n.i)(u.v)(a.|mkset nth(v,i)|)) mult_nthcdr mc3)
    ;MULT(NTHCDR(V,I),MKSET(NTH(V,I)))≤MULT(V,MKSET(NTH(V,I)))
    ;deps: (MC0 MC1)

    ;labels: TRANS_LESSEQ 
    ;∀N M K.N≤M∧M≤K⊃N≤K

10. (ue ((n.|2|)
         (m.|mult(nthcdr(v,i),mkset nth(v,i))|)
         (k.|mult(v,mkset nth(v,i))|))
        trans_lesseq mc6 *)

11. (ci (mc1 mc0 mc2))
    ;I<J∧J<LENGTH V∧NTH(V,I)=NTH(V,J)⊃2≤MULT(V,MKSET(NTH(V,I)))
;lemma multiplicity implies injectivity
(proof mult_inj)

1.  (assume |∀k.k<length v⊃mult(v,mkset(nth(v,k)))=1|)
    (label mi1)

2.  (assume |i<length v∧j<length v∧nth(v,i)=nth(v,j)|)
    (label mi2)

3.  (ue ((v.v)(i.i)(j.j)) multinj_computation mi2
        (use mi1 ue: ((k.i)) mode: exact)(open lesseq))
    ;¬I<J
    ;deps: (MI1 MI2)

4.  (ue ((v.v)(i.j)(j.i)) multinj_computation mi2
        (use mi1 ue: ((k.j)) mode: exact)(open lesseq))
    ;¬J<I
    ;deps: (MI1 MI2)

5.  (derive |i=j| (trichotomy * -2))
    ;deps: (MI1 MI2)

6.  (ci mi2)
    ;I<LENGTH V∧J<LENGTH V∧NTH(V,I)=NTH(V,J)⊃I=J
    ;deps: (MI1)

7.  (trw |inj v| (open inj) *)
    ;INJ(V)
    ;deps: (MI1)

8.  (ci mi1)
    ;(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)
;proof multsum                                
;Lemma:if disjoint union, the mult. of the union is the sum of the multiplicities

    (wipe-out)
    (get-proofs mult prf ekl sys)
    (proof multsum)

1.  (ue (phi |λu. disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|) listinduction
        (part 1 (open mult union disj_pair emptyp intersection) 
                (use normal mode: always)) 
        (part 1 (der)) )
    ;∀U.DISJ_PAIR(A,B)⊃MULT(U,A∪B)=MULT(U,A)+MULT(U,B)
    (label multsum)

;LEMMA
;∀U.DISJ_PAIR(A,B)⊃MULT(U,A∪B)=MULT(U,A)+MULT(U,B)

;Proof: By induction on U. For U = NIL, all values of mult are 0. Assume it for U,
;want it for X.U. The assumption that A and B are disjoint means that the intersection 
;of A and B is EMPTYP, i.e. that for no X, Xε A and XεB. If not XεA and not XεB
;then induction hypothesis gives the result. If XεA or XεB, then by disjointness
;if xεA then ¬xεB, else XεB and in both cases 
;mult(X.U,A∪B)=mult(U,A∪B)'=(mult(U,A)+mult(U,B))'=mult(X.U,A)+mult(X.U,B)
;(-the induction hypothesis is used to establish the second equality-)
;Lemma:if disjoint-set,then multiplicity of union = sum of the multiplicities

    (proof mult_of_un_is_sum_mult)

1.  (ue (a |λn.disjoint(setseq,n)⊃mult(u,un(setseq,n))=sum(λx1.mult(u,setseq(x1)),n)|)
        proof_by_induction (open disjoint un sum mult ) multfact
	(use multsum mode: exact) (use normal mode: always))
    ;∀N.DISJOINT(SETSEQ,N)⊃MULT(U,UN(SETSEQ,N))=SUM(λX1.MULT(U,SETSEQ(X1)),N)



;LEMMA
;∀N.DISJOINT(SETSEQ,N)⊃mult(U,UN(SETSEQ,N))=SUM(λX1.mult(U,SETSEQ(X1)),N)

;Proof: By induction on N. For N=0, UN(SETSEQ,0) is EMPTYSET, whose mult in 0 (simpinfo),
;and SUM(...,0) is 0 too. Assume the result for N.
;DISJOINT(SETSEQ,N')
;                    implies
;DISJOINT(SETSEQ,N)
;                    By DISJOINTFACT, it follows 
;DISJ_PAIR(UN(SETSEQ,N),SETSEQ(N))      
;                    which implies, using multSUM
;mult(U,UN(SETSEQ,N)∪SETSEQ(N))=mult(U,UN(SETSEQ,N))+mult(U,SETSEQ(N))
;                    which is, by definition of UN and induction hypothesis
;mult(U,UN(SETSEQ,N'))=SUM(λX1.mult(U,SETSEQ(X1)),N)+mult(U,SETSEQ(N))
;                    i.e. by definition of sum
;mult(U,UN(SETSEQ,N'))=SUM(λX1.mult(U,SETSEQ(X1)),N')